Nuprl Lemma : Tactics as terms |
13,42 |
|
ABS: skip{a}
ABS: let $x = a in b
ABS: THENL(a; l)
ABS: (a THENM b)
ABS: (a THENA b)
ABS: (a THEN b)
ABS: (a ORELSE b)
ABS: (Assert a BY b)
ABS: Decide a
ABS: Try (a)
ABS: Complete (a)
ABS: RepeatFor $n (a)
ABS: SplitOnHypITE $n
ABS: HypSubst' $dir $a $b
ABS: Subst' x $b
ABS: BHyp $a
ABS: D $a
ABS: ExRepD
ABS: Auto
ABS: MaAuto
ABS: Unfold `$ab` $hyp
ABS: Unfolds ``$abs`` $hyp
ABS: RepUR ``$abs`` $hyp
ABS: ParallelOp $hyp
ABS: Branch3
ABS: Branch2
ABS: OnMaybeHyp $h (\h. tactic)
ABS: EsReal `$opid` tokens